| Definitions | Normal(T),  b,  x dom(f). v=f(x)   P(x;v), Normal(ds), False,  A, Type,  , t T,  x.A(x), Id, x:A. B(x), P Q, IdDeq, P  Q, P & Q, P Q,  x,y. t(x;y), x. t(x), left + right, Knd, x:A  B(x), a:A fp B(a), IdLnk, Atom$n, x:A B(x), s = t, k(v:B) sends on l [tg:T, f <state, v>]?[], if b then t else f fi , tag(k), x : v,  , Unit, Void, case b of inl(x) => s(x) | inr(y) => t(y), DeclaredType(ds;x), <a, b>,  b, f  g, lnk(k), State(ds), type List, (x l), {x:A| B(x)} , [], Top, f(x)?z,  x:A.B(x), S  T, suptype(S; T), do-apply(f;x), [car / cdr], can-apply(f;x), isrcvl(l;k), ES,  es.P(es), EqDecider(T), EOrderAxioms(E; pred?; info), f(a), EState(T), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M),  ,  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r  s, constant_function(f;A;B), pred!(e;e'), SWellFounded(R(x;y)), first(e), loc(e), kind(e), sends k(v:T) on l:tagged(g,State(ds),v):dt, rcv(l,tg), source(l), destination(l), isrcv(k), a = b, {T}, a = b, x dom(f), SQType(T), s ~ t |
| Lemmas | fpf-single-dom, isrcv-implies, IdLnk sq, Id sq, fpf-dom wf, sends-p-implies-conditional-send-p, not functionality wrt iff, assert-eq-knd, eq knd wf, implies functionality wrt iff, assert-eq-id, eq id wf, normal-ds wf, normal-type wf, isrcv wf, ldst wf, lsrc wf, Knd wf, rcv wf, es-real-monotonicity, event system wf, sends-p wf, deq wf, EOrderAxioms wf, kind wf, loc wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, rationals wf, kindcase wf, EState wf, constant function wf, first wf, unit wf, conditional-send-p wf, sends-p-realizable, isrcvl wf, bool wf, decl-state wf, can-apply wf, fpf wf, do-apply wf, subtype rel function, fpf-cap-single1, subtype rel sum, fpf-join-cap-sq, fpf-cap-single, fpf-single-dom-sq, eqof eq btrue, fpf-cap-single-join, fpf-cap wf, top wf, ifthenelse wf, decl-type wf, fpf-join wf, fpf-single wf, assert-eq-lnk, IdLnk wf, lnk wf, bnot wf, not wf, assert wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-all-join-decl, fpf-single wf3, fpf-all-single-decl, tagof wf, assert-isrcvl, fpf-all-single, Id wf, id-deq wf |